\begin{tabbing}
$\forall$\=$T$:Type, $t$:$T$, $p$:FinProbSpace, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow\mathbb{B}$),\+
\\[0ex]$f$:(\{$s$:State(${\it ds}$)$\mid$ $\uparrow$($P$($s$))\} $\rightarrow$Outcome$\rightarrow$$T$).
\-\\[0ex]Normal(${\it ds}$) $\Rightarrow$ $\vdash$${\it es}$.weak{-}precond{-}send{-}p(${\it es}$;$T$;Outcome;$l$;"tg";"a";${\it ds}$;$P$;$f$)
\end{tabbing}